WellFnd{i}(A;x,y.R(x;y)) == P:(A). (j:A. (k:A. R(k;j)  P(k))  P(j))  {n:A. P(n)} 

latex

---

clarification:

WellFnd{i}(A;x,y.R(x;y))
== P:(A{i}). (j:A. (k:A. R(k;j)  P(k))  P(j))  {n:A. P(n)} 

latex

Up	well fnd, well fnd
Wellformedness Lemmas	wellfounded wf, wellfounded wf
Definitions	x:AB(x), , P  Q, {T}, x:A. B(x), x(s)
FDL editor aliases	wellfounded